<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Issue6276</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Markup">\begin{code}</a>
<a id="14" class="Keyword">record</a> <a id="R"></a><a id="21" href="Issue6276.html#21" class="Record">R</a> <a id="23" class="Symbol">(</a><a id="24" href="Issue6276.html#24" class="Bound">A</a> <a id="26" class="Symbol">:</a> <a id="28" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="31" class="Symbol">)</a> <a id="33" class="Symbol">:</a> <a id="35" href="Agda.Primitive.html#388" class="Primitive">Set</a>

<a id="40" class="Keyword">record</a> <a id="47" href="Issue6276.html#21" class="Record">R</a> <a id="49" href="Issue6276.html#49" class="Bound">A</a> <a id="51" class="Keyword">where</a>
<a id="57" class="Markup">\end{code}</a><a id="67" class="Background">
</a></pre></body></html>